1  /-
  2  Copyright (c) 2019 Chris Hughes. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Chris Hughes
  5  -/
  6  
  7  import ring_theory.noetherian linear_algebra.dimension
src         └────────────────────┘ └──────────────────────┘
  8  import ring_theory.principal_ideal_domain
src         └────────────────────────────────┘
  9  
 10  /-!
 11  # Finite dimensional vector spaces
 12  
 13  Definition and basic properties of finite dimensional vector spaces, of their dimensions, and
 14  of linear maps on such spaces.
 15  
 16  ## Main definitions
 17  
 18  Assume `V` is a vector space over a field `K`. There are (at least) three equivalent definitions of
 19  finite-dimensionality of `V`:
 20  
 21  - it admits a finite basis.
 22  - it is finitely generated.
 23  - it is noetherian, i.e., every subspace is finitely generated.
 24  
 25  We introduce a typeclass `finite_dimensional K V` capturing this property. For ease of transfer of
 26  proof, it is defined using the third point of view, i.e., as `is_noetherian`. However, we prove
 27  that all these points of view are equivalent, with the following lemmas
 28  (in the namespace `finite_dimensional`):
 29  
 30  - `exists_is_basis_finite` states that a finite-dimensional vector space has a finite basis
 31  - `of_finite_basis` states that the existence of a finite basis implies finite-dimensionality
 32  - `iff_fg` states that the space is finite-dimensional if and only if it is finitely generated
 33  
 34  Also defined is `findim`, the dimension of a finite dimensional space, returning a `nat`,
 35  as opposed to `dim`, which returns a `cardinal`. When the space has infinite dimension, its
 36  `findim` is by convention set to `0`.
 37  
 38  Preservation of finite-dimensionality and formulas for the dimension are given for
 39  - submodules
 40  - quotients (for the dimension of a quotient, see `findim_quotient_add_findim`)
 41  - linear equivs, in `linear_equiv.finite_dimensional` and `linear_equiv.findim_eq`
 42  - image under a linear map (the rank-nullity formula is in `findim_range_add_findim_ker`)
 43  
 44  Basic properties of linear maps of a finite-dimensional vector space are given. Notably, the
 45  equivalence of injectivity and surjectivity is proved in `linear_map.injective_iff_surjective`,
 46  and the equivalence between left-inverse and right-inverse in `mul_eq_one_comm` and
 47  `comp_eq_id_comm`.
 48  
 49  ## Implementation notes
 50  
 51  Most results are deduced from the corresponding results for the general dimension (as a cardinal),
 52  in `dimension.lean`. Not all results have been ported yet.
 53  
 54  One of the characterizations of finite-dimensionality is in terms of finite generation. This
 55  property is currently defined only for submodules, so we express it through the fact that the
 56  maximal submodule (which, as a set, coincides with the whole space) is finitely generated. This is
 57  not very convenient to use, although there are some helper functions. However, this becomes very
 58  convenient when speaking of submodules which are finite-dimensional, as this notion coincides with
 59  the fact that the submodule is finitely generated (as a submodule of the whole space). This
 60  equivalence is proved in `submodule.fg_iff_finite_dimensional`.
 61  -/
 62  
 63  universes u v v' w
 64  open_locale classical
 65  
 66  open vector_space cardinal submodule module function
 67  
 68  variables {K : Type u} {V : Type v} [discrete_field K] [add_comm_group V] [vector_space K V]
id                                        └────────────┘     └────────────┘     └──────────┘
src                                       └────────────┘     └────────────┘     └──────────┘
typ                                       └────────────┘     └────────────┘     └──────────┘
doc                                                                             └──────────┘
 69  {V₂ : Type v'} [add_comm_group V₂] [vector_space K V₂]
id                   └────────────┘      └──────────┘
src                  └────────────┘      └──────────┘
typ                  └────────────┘      └──────────┘
doc                                      └──────────┘
 70  
 71  /-- `finite_dimensional` vector spaces are defined to be noetherian modules.
 72  Use `finite_dimensional.iff_fg` or `finite_dimensional.of_finite_basis` to prove finite dimension
 73  from a conventional definition. -/
 74  @[reducible] def finite_dimensional (K V : Type*) [discrete_field K]
id                                                      └────────────┘ 
src                                                     └────────────┘
typ                                                     └────────────┘ 
doc    └───────┘
 75    [add_comm_group V] [vector_space K V] := is_noetherian K V
id      └────────────┘    └──────────┘       └───────────┘  
src     └────────────┘     └──────────┘         └───────────┘
typ     └────────────┘    └──────────┘       └───────────┘  
doc                        └──────────┘
 76  
 77  namespace finite_dimensional
 78  
 79  open is_noetherian
 80  
 81  /-- A vector space is finite-dimensional if and only if its dimension (as a cardinal) is strictly
 82  less than the first infinite cardinal `omega`. -/
 83  lemma finite_dimensional_iff_dim_lt_omega : finite_dimensional K V ↔ dim K V < omega.{v} :=
id                                               └────────────────┘    └─┘    └───┘
src                                              └────────────────┘      └─┘      └───┘
typ                                              └────────────────┘    └─┘    └───┘
doc                                              └────────────────┘                 └───┘
 84  begin
st   └─────
 85    cases exists_is_basis K V with b hb,
id           └─────────────┘  
src    └────┘└─────────────┘  └────────┘
typ    └────┘└─────────────┘└────────┘
doc    └────┘                 └────────┘
txt    └────┘                 └────────┘
par    └────┘                 └────────┘
pid                          └────────┘
st   ────────────────────────────────────┘└─
 86    have := is_basis.mk_eq_dim hb,
id             └────────────────┘ └┘
src    └──────┘└────────────────┘
typ    └──────┘└────────────────┘└┘
doc    └──────┘                  
txt    └──────┘                  
par    └──────┘                  
pid    └───┘└─┘                  
st   ──────────────────────────────┘└─
 87    simp only [lift_id] at this,
id                └─────┘
src    └─────────┘└─────┘└───────┘
typ    └─────────┘└─────┘└───────┘
doc    └─────────┘       └───────┘
txt    └─────────┘       └───────┘
par    └─────────┘       └───────┘
pid        └──┘└┘       └─────┘
st   ────────────────────────────┘└─
 88    rw [← this, lt_omega_iff_fintype, ← @set.set_of_mem_eq _ b, ← subtype.val_range],
id           └──┘  └──────────────────┘     └───────────────┘       └───────────────┘
src    └────┘    └┘└──────────────────┘└──┘ └───────────────┘└─┘ └──┘└───────────────┘
typ    └────┘└──┘└┘└──────────────────┘└──┘ └───────────────┘└─┘└──┘└───────────────┘
doc    └────┘    └┘                    └──┘                  └─┘ └──┘                 
txt    └────┘    └┘                    └──┘                  └─┘ └──┘                 
par    └────┘    └┘                    └──┘                  └─┘ └──┘                 
pid      └──┘    └┘                    └──┘                  └─┘ └──┘                 
st   ───────────┘└────────────────────┘└────────────────────────┘└───────────────────┘└──
 89    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
 90    { intro, resetI, convert finite_of_linear_independent hb.1, simp },
id                              └──────────────────────────┘ └┘
src      └───┘  └────┘  └──────┘└──────────────────────────┘  └┘  └───┘
typ      └───┘  └────┘  └──────┘└──────────────────────────┘└┘└┘  └───┘
doc      └───┘  └────┘  └──────┘                              └┘  └───┘
txt      └───┘  └────┘  └──────┘                              └┘  └───┘
par      └───┘  └────┘  └──────┘                              └┘  └───┘
pid                                                          └┘      
st   ───┘└───┘└─────────────────────────────────────────────────┘└─────┘└┘
 91    { assume hbfinite,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid      └─────────────┘
st   ──────────────────┘└─
 92      refine @is_noetherian_of_linear_equiv K (⊤ : submodule K V) V _
id               └───────────────────────────┘       └───────┘     
src      └─────┘ └───────────────────────────┘  └─┘└───────┘  └┘ └──
typ      └─────┘ └───────────────────────────┘  └─┘└───────┘ └┘└──
doc      └─────┘                                 └─┘└───────┘  └┘ └──
txt      └─────┘                                 └─┘           └┘ └──
par      └─────┘                                 └─┘           └┘ └──
pid                                             └─┘           └┘ └──
st   ────────────────────────────────────────────────────────────────────
 93        _ _ _ _ (linear_equiv.of_top _ rfl) (id _),
id                  └─────────────────┘   └─┘   └┘
src  ─────────────┘ └─────────────────┘└─┘└─┘└┘ └┘└─┘
typ  ─────────────┘ └─────────────────┘└─┘└─┘└┘ └┘└─┘
doc  ─────────────┘ └─────────────────┘└─┘   └┘   └─┘
txt  ─────────────┘                    └─┘   └┘   └─┘
par  ─────────────┘                    └─┘   └┘   └─┘
pid  ─────────────┘                    └─┘   └┘   └─┘
st   ───────────────────────────────────────────────┘└─
 94      refine is_noetherian_of_fg_of_noetherian _ ⟨set.finite.to_finset hbfinite, _⟩,
id              └───────────────────────────────┘    └──────────────────┘ └──────┘
src      └─────┘└───────────────────────────────┘└─┘ └──────────────────┘        └──┘
typ      └─────┘└───────────────────────────────┘└─┘ └──────────────────┘└──────┘└──┘
doc      └─────┘                                 └─┘ └──────────────────┘        └──┘
txt      └─────┘                                 └─┘                             └──┘
par      └─────┘                                 └─┘                             └──┘
pid                                             └─┘                             └──┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
 95      rw [set.finite.coe_to_finset, ← hb.2], refl }
id           └──────────────────────┘    └┘
src      └──┘└──────────────────────┘└──┘  └─┘  └───┘
typ      └──┘└──────────────────────┘└──┘└┘└─┘  └───┘
doc      └──┘                        └──┘  └─┘  └───┘
txt      └──┘                        └──┘  └─┘  └───┘
par      └──┘                        └──┘  └─┘  └───┘
pid        └┘                        └──┘  └─┘      
st   ───────────────────────────────┘└────┘└────────┘└─
 96  end
st   ──┘
 97  
 98  /-- The dimension of a finite-dimensional vector space, as a cardinal, is strictly less than the
 99  first infinite cardinal `omega`. -/
100  lemma dim_lt_omega (K V : Type*) [discrete_field K] [add_comm_group V] [vector_space K V] :
id                                     └────────────┘    └────────────┘    └──────────┘  
src                                    └────────────┘     └────────────┘     └──────────┘
typ                                    └────────────┘    └────────────┘    └──────────┘  
doc                                                                          └──────────┘
101    ∀ [finite_dimensional K V], dim K V < omega.{v} :=
id        └────────────────┘     └─┘    └───┘
src       └────────────────┘       └─┘      └───┘
typ       └────────────────┘     └─┘    └───┘
doc       └────────────────┘                 └───┘
102  finite_dimensional_iff_dim_lt_omega.1
id   └─────────────────────────────────┘
src  └─────────────────────────────────┘
typ  └─────────────────────────────────┘
doc  └─────────────────────────────────┘
103  
104  /-- In a finite dimensional space, there exists a finite basis. A basis is in general given as a
st                                  
105  function from an arbitrary type to the vector space. Here, we think of a basis as a set (instead of
st                  
106  a function), and use as parametrizing type this set (and as a function the function `subtype.val`).
107  -/
108  variables (K V)
109  lemma exists_is_basis_finite [finite_dimensional K V] :
id                                 └────────────────┘  
src                                └────────────────┘
typ                                └────────────────┘  
doc                                └────────────────┘
110    ∃ s : set V, (is_basis K (subtype.val : s → V)) ∧ s.finite :=
id          └─┘   └──────┘   └─────────┘          └─────┘
src         └─┘    └──────┘    └─────────┘             └─────┘
typ         └─┘   └──────┘   └─────────┘          └─────┘
doc                  └──────┘                             └─────┘
111  begin
st   └─────
112    cases exists_is_basis K V with s hs,
id           └─────────────┘  
src    └────┘└─────────────┘  └────────┘
typ    └────┘└─────────────┘└────────┘
doc    └────┘                 └────────┘
txt    └────┘                 └────────┘
par    └────┘                 └────────┘
pid                          └────────┘
st   ────────────────────────────────────┘└─
113    exact ⟨s, hs, finite_of_linear_independent hs.1⟩
id                  └──────────────────────────┘ └┘
src    └────┘  └┘  └┘└──────────────────────────┘  └──┘
typ    └────┘ └┘  └┘└──────────────────────────┘└┘└──┘
doc    └────┘  └┘  └┘                              └──┘
txt    └────┘  └┘  └┘                              └──┘
par    └────┘  └┘  └┘                              └──┘
pid           └┘  └┘                              └─┘
st   ──────────────────────────────────────────────────┘
114  end
st   └─┘
115  variables {K V}
116  
117  /-- A vector space is finite-dimensional if and only if it is finitely generated. As the
118  finitely-generated property is a property of submodules, we formulate this in terms of the
119  maximal submodule, equal to the whole space as a set by definition.-/
120  lemma iff_fg :
121    finite_dimensional K V ↔ (⊤ : submodule K V).fg :=
id     └────────────────┘        └───────┘   └┘
src    └────────────────┘          └───────┘     └┘
typ    └────────────────┘        └───────┘   └┘
doc    └────────────────┘            └───────┘
122  begin
st   └─────
123    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
124    { introI h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid            └┘
st   ───┘└──────┘└─
125      rcases exists_is_basis_finite K V with ⟨s, s_basis, s_finite⟩,
id              └────────────────────┘  
src      └─────┘└────────────────────┘  └──────────────────────────┘
typ      └─────┘└────────────────────┘└──────────────────────────┘
doc      └─────┘                        └──────────────────────────┘
txt      └─────┘                        └──────────────────────────┘
par      └─────┘                        └──────────────────────────┘
pid                                    └──────────────────────────┘
st   ────────────────────────────────────────────────────────────────┘└─
126      exact ⟨s_finite.to_finset, by { convert s_basis.2, simp }⟩ },
id              └────────────────┘               └─────┘
src      └────┘ └────────────────┘└┘  └─┘└──────┘       └┘└┘└───┘└─┘
typ      └────┘ └────────────────┘└┘  └─┘└──────┘└─────┘└┘└┘└───┘└─┘
doc      └────┘ └────────────────┘└┘  └─┘└──────┘       └┘└┘└───┘└─┘
txt      └────┘                   └┘  └─┘└──────┘       └┘└┘└───┘└─┘
par      └────┘                   └┘  └─┘└──────┘       └┘└┘└───┘└─┘
pid                              └┘  └─────────┘       └─────────┘
st   ────────────────────────────────┘└──────────────────┘└─────┘└┘└┘
127    { rintros ⟨s, hs⟩,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid             └──────┘
st   ──────────────────┘└─
128      rw [finite_dimensional_iff_dim_lt_omega, ← dim_top, ← hs],
id           └─────────────────────────────────┘    └─────┘    └┘
src      └──┘└─────────────────────────────────┘└──┘└─────┘└──┘  
typ      └──┘└─────────────────────────────────┘└──┘└─────┘└──┘└┘
doc      └──┘└─────────────────────────────────┘└──┘       └──┘  
txt      └──┘                                   └──┘       └──┘  
par      └──┘                                   └──┘       └──┘  
pid        └┘                                   └──┘       └──┘  
st   ──────────────────────────────────────────┘└─────────┘└────┘└──
129      exact lt_of_le_of_lt (dim_span_le _) (lt_omega_iff_finite.2 (set.finite_mem_finset s)) }
id             └────────────┘  └─────────┘     └─────────────────┘    └───────────────────┘ 
src      └────┘└────────────┘ └─────────┘└──┘ └─────────────────┘└─┘ └───────────────────┘ └─┘
typ      └────┘└────────────┘ └─────────┘└──┘ └─────────────────┘└─┘ └───────────────────┘└─┘
doc      └────┘                          └──┘                    └─┘                       └─┘
txt      └────┘                          └──┘                    └─┘                       └─┘
par      └────┘                          └──┘                    └─┘                       └─┘
pid                                     └──┘                    └─┘                       └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
130  end
st   ──┘
131  
132  /-- If a vector space has a finite basis, then it is finite-dimensional. -/
133  lemma of_finite_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K b) :
id                                       └─────┘                  └──────┘  
src                                      └─────┘                     └──────┘
typ                                      └─────┘                  └──────┘  
doc                                      └─────┘                     └──────┘
134    finite_dimensional K V :=
id     └────────────────┘  
src    └────────────────┘
typ    └────────────────┘  
doc    └────────────────┘
135  iff_fg.2 $ ⟨finset.univ.image b, by {convert h.2, simp} ⟩
id   └────┘     └─────────┘└────┘               
src  └────┘     └─────────┘└────┘        └──────┘ └┘  └──┘
typ  └────┘     └─────────┘└────┘       └──────┘└┘  └──┘
doc  └────┘      └─────────┘└────┘        └──────┘ └┘  └──┘
txt                                       └──────┘ └┘  └──┘
par                                       └──────┘ └┘  └──┘
pid                                               └┘
st                                      └───────────┘└────┘└┘
136  
137  /-- A subspace of a finite-dimensional space is also finite-dimensional. -/
138  instance finite_dimensional_submodule [finite_dimensional K V] (S : submodule K V) :
id                                          └────────────────┘         └───────┘  
src                                         └────────────────┘           └───────┘
typ                                         └────────────────┘         └───────┘  
doc                                         └────────────────┘           └───────┘
139    finite_dimensional K S :=
id     └────────────────┘  
src    └────────────────┘
typ    └────────────────┘  
doc    └────────────────┘
140  finite_dimensional_iff_dim_lt_omega.2 (lt_of_le_of_lt (dim_submodule_le _) (dim_lt_omega K V))
id   └─────────────────────────────────┘   └────────────┘  └──────────────┘     └──────────┘  
src  └─────────────────────────────────┘   └────────────┘  └──────────────┘     └──────────┘
typ  └─────────────────────────────────┘   └────────────┘  └──────────────┘     └──────────┘  
doc  └─────────────────────────────────┘                                         └──────────┘
141  
142  /-- A quotient of a finite-dimensional space is also finite-dimensional. -/
143  instance finite_dimensional_quotient [finite_dimensional K V] (S : submodule K V) :
id                                         └────────────────┘         └───────┘  
src                                        └────────────────┘           └───────┘
typ                                        └────────────────┘         └───────┘  
doc                                        └────────────────┘           └───────┘
144    finite_dimensional K (quotient S) :=
id     └────────────────┘   └──────┘ 
src    └────────────────┘    └──────┘
typ    └────────────────┘   └──────┘ 
doc    └────────────────┘    └──────┘
145  finite_dimensional_iff_dim_lt_omega.2 (lt_of_le_of_lt (dim_quotient_le _) (dim_lt_omega K V))
id   └─────────────────────────────────┘   └────────────┘  └─────────────┘     └──────────┘  
src  └─────────────────────────────────┘   └────────────┘  └─────────────┘     └──────────┘
typ  └─────────────────────────────────┘   └────────────┘  └─────────────┘     └──────────┘  
doc  └─────────────────────────────────┘                                        └──────────┘
146  
147  /-- The dimension of a finite-dimensional vector space as a natural number. Defined by convention to
148  be `0` if the space is infinite-dimensional. -/
149  noncomputable def findim (K V : Type*) [discrete_field K]
id                                           └────────────┘ 
src                                          └────────────┘
typ                                          └────────────┘ 
150    [add_comm_group V] [vector_space K V] : ℕ :=
id      └────────────┘    └──────────┘      
src     └────────────┘     └──────────┘        
typ     └────────────┘    └──────────┘      
doc                        └──────────┘
151  if h : dim K V < omega.{v} then classical.some (lt_omega.1 h) else 0
id   └┘     └─┘    └───┘          └────────────┘  └──────┘         
src  └┘     └─┘      └───┘          └────────────┘  └──────┘          
typ  └┘     └─┘    └───┘          └────────────┘  └──────┘         
doc                   └───┘
152  
153  /-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its `findim`. -/
154  lemma findim_eq_dim (K : Type u) (V : Type v) [discrete_field K]
id                                                  └────────────┘ 
src                                                 └────────────┘
typ                                                 └────────────┘ 
155    [add_comm_group V] [vector_space K V] [finite_dimensional K V] :
id      └────────────┘    └──────────┘     └────────────────┘  
src     └────────────┘     └──────────┘       └────────────────┘
typ     └────────────┘    └──────────┘     └────────────────┘  
doc                        └──────────┘       └────────────────┘
156    (findim K V : cardinal.{v}) = dim K V :=
id      └────┘     └──────┘       └─┘  
src     └────┘       └──────┘       └─┘
typ     └────┘     └──────┘       └─┘  
doc     └────┘       └──────┘
157  begin
st   └─────
158    have : findim K V = classical.some (lt_omega.1 (dim_lt_omega K V)) :=
id            └────┘      └────────────┘  └──────┘    └──────────┘  
src    └─────┘└────┘  └────────────┘ └──────┘└─┘ └──────────┘  └─────
typ    └─────┘└────┘  └────────────┘ └──────┘└─┘ └──────────┘└─────
doc    └─────┘└────┘                          └─┘ └──────────┘  └─────
txt    └─────┘                                └─┘               └─────
par    └─────┘                                └─┘               └─────
pid    └───┘└┘                                └─┘               └┘└───
st   ────────────────────────────────────────────────────────────────────────
159      dif_pos (dim_lt_omega K V),
id       └─────┘  └──────────┘  
src  ───┘└─────┘ └──────────┘  
typ  ───┘└─────┘ └──────────┘
doc  ───┘        └──────────┘  
txt  ───┘                      
par  ───┘                      
pid  ───┘                      
st   ─────────────────────────────┘└─
160    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
161    exact (classical.some_spec (lt_omega.1 (dim_lt_omega K V))).symm
id            └─────────────────┘  └──────┘    └──────────┘  
src    └────┘ └─────────────────┘ └──────┘└─┘ └──────────┘  └───────┘
typ    └────┘ └─────────────────┘ └──────┘└─┘ └──────────┘└───────┘
doc    └────┘                             └─┘ └──────────┘  └───────┘
txt    └────┘                             └─┘               └───────┘
par    └────┘                             └─┘               └───────┘
pid                                      └─┘               └─────┘└┘
st   ──────────────────────────────────────────────────────────────────┘
162  end
st   └─┘
163  
164  /-- If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the
165  cardinality of the basis. -/
166  lemma dim_eq_card_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K b) :
id                                         └─────┘                  └──────┘  
src                                        └─────┘                     └──────┘
typ                                        └─────┘                  └──────┘  
doc                                        └─────┘                     └──────┘
167    dim K V = fintype.card ι :=
id     └─┘    └──────────┘ 
src    └─┘      └──────────┘
typ    └─┘    └──────────┘ 
doc              └──────────┘
168  by rw [←h.mk_range_eq_dim, cardinal.fintype_card,
id                              └───────────────────┘
src     └───┘                 └┘└───────────────────┘└─
typ     └───┘└───────────────┘└┘└───────────────────┘└─
doc     └───┘                 └┘                     └─
txt     └───┘                 └┘                     └─
par     └───┘                 └┘                     └─
pid       └─┘                 └┘                     └─
st     └─────────────────────┘└─────────────────────┘└─
169         set.card_range_of_injective (h.injective zero_ne_one)]
id          └─────────────────────────┘  └─────────┘ └─────────┘
src  ──────┘└─────────────────────────┘ └─────────┘└─────────┘└──
typ  ──────┘└─────────────────────────┘ └─────────┘└─────────┘└──
doc  ──────┘                                                  └──
txt  ──────┘                                                  └──
par  ──────┘                                                  └──
pid  ──────┘                                                  └┘
st   ───────────────────────────────────────────────────────────┘
170  
src  
typ  
doc  
txt  
par  
pid  
st   
171  
src  
typ  
doc  
txt  
par  
pid  
st   
172  /-- If a vector space has a finite basis, then its dimension is equal to the cardinality of the
173  basis. -/
174  lemma findim_eq_card_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K b) :
id                                            └─────┘                  └──────┘  
src                                           └─────┘                     └──────┘
typ                                           └─────┘                  └──────┘  
doc                                           └─────┘                     └──────┘
175    findim K V = fintype.card ι :=
id     └────┘    └──────────┘ 
src    └────┘      └──────────┘
typ    └────┘    └──────────┘ 
doc    └────┘       └──────────┘
176  begin
st   └─────
177    haveI : finite_dimensional K V := of_finite_basis h,
id             └────────────────┘      └─────────────┘ 
src    └──────┘└────────────────┘  └──┘└─────────────┘
typ    └──────┘└────────────────┘└──┘└─────────────┘
doc    └──────┘└────────────────┘  └──┘└─────────────┘
txt    └──────┘                    └──┘               
par    └──────┘                    └──┘               
pid         └┘                    └──┘               
st   ────────────────────────────────────────────────────┘└─
178    have := dim_eq_card_basis h,
id             └───────────────┘ 
src    └──────┘└───────────────┘
typ    └──────┘└───────────────┘
doc    └──────┘└───────────────┘
txt    └──────┘                 
par    └──────┘                 
pid    └───┘└─┘                 
st   ────────────────────────────┘└─
179    rw ← findim_eq_dim at this,
id          └───────────┘
src    └───┘└───────────┘└──────┘
typ    └───┘└───────────┘└──────┘
doc    └───┘└───────────┘└──────┘
txt    └───┘             └──────┘
par    └───┘             └──────┘
pid      └─┘             └──────┘
st   ───────────────────────────┘└─
180    exact_mod_cast this
id                    └──┘
src    └─────────────┘    
typ    └─────────────┘└──┘
doc    └─────────────┘    
txt    └─────────────┘    
par    └─────────────┘    
pid                      
st   ─────────────────────┘
181  end
st   └─┘
182  
183  /-- If a vector space is finite-dimensional, then the cardinality of any basis is equal to its
184  `findim`. -/
185  lemma findim_eq_card_basis' [finite_dimensional K V] {ι : Type w} {b : ι → V} (h : is_basis K b) :
id                                └────────────────┘                                └──────┘  
src                               └────────────────┘                                    └──────┘
typ                               └────────────────┘                                └──────┘  
doc                               └────────────────┘                                    └──────┘
186    (findim K V : cardinal.{w}) = cardinal.mk ι  :=
id      └────┘     └──────┘       └─────────┘ 
src     └────┘       └──────┘       └─────────┘
typ     └────┘     └──────┘       └─────────┘ 
doc     └────┘       └──────┘        └─────────┘
187  begin
st   └─────
188    rcases exists_is_basis_finite K V with ⟨s, s_basis, s_finite⟩,
id            └────────────────────┘  
src    └─────┘└────────────────────┘  └──────────────────────────┘
typ    └─────┘└────────────────────┘└──────────────────────────┘
doc    └─────┘                        └──────────────────────────┘
txt    └─────┘                        └──────────────────────────┘
par    └─────┘                        └──────────────────────────┘
pid                                  └──────────────────────────┘
st   ──────────────────────────────────────────────────────────────┘└─
189    letI: fintype s := s_finite.fintype,
id           └─────┘     └──────────────┘
src    └────┘└─────┘ └──┘└──────────────┘
typ    └────┘└─────┘└──┘└──────────────┘
doc    └────┘└─────┘ └──┘└──────────────┘
txt    └────┘        └──┘
par    └────┘        └──┘
pid        └┘        └──┘
st   ────────────────────────────────────┘└─
190    have A : cardinal.mk s = fintype.card s := fintype_card _,
id              └─────────┘    └──────────┘     └──────────┘
src    └───────┘└─────────┘ └──────────┘ └──┘└──────────┘└┘
typ    └───────┘└─────────┘ └──────────┘└──┘└──────────┘└┘
doc    └───────┘└─────────┘  └──────────┘ └──┘            └┘
txt    └───────┘                          └──┘            └┘
par    └───────┘                          └──┘            └┘
pid    └────┘└─┘                          └──┘            └┘
st   ──────────────────────────────────────────────────────────┘└─
191    have B : findim K V = fintype.card s := findim_eq_card_basis s_basis,
id              └────┘     └──────────┘     └──────────────────┘ └─────┘
src    └───────┘└────┘   └──────────┘ └──┘└──────────────────┘
typ    └───────┘└────┘ └──────────┘└──┘└──────────────────┘└─────┘
doc    └───────┘└────┘   └──────────┘ └──┘└──────────────────┘
txt    └───────┘                      └──┘                    
par    └───────┘                      └──┘                    
pid    └────┘└─┘                      └──┘                    
st   ─────────────────────────────────────────────────────────────────────┘└─
192    have C : cardinal.lift.{w v} (cardinal.mk ι) = cardinal.lift.{v w} (cardinal.mk s) :=
id              └───────────┘                        └───────────┘        └─────────┘ 
src    └───────┘└───────────┘└─────┘             └┘ └───────────┘└─────┘ └─────────┘ └────
typ    └───────┘└───────────┘└─────┘            └┘ └───────────┘└─────┘ └─────────┘└────
doc    └───────┘└───────────┘└─────┘             └┘ └───────────┘└─────┘ └─────────┘ └────
txt    └───────┘             └─────┘             └┘              └─────┘             └────
par    └───────┘             └─────┘             └┘              └─────┘             └────
pid    └────┘└─┘             └─────┘             └┘              └─────┘             └───
st   ────────────────────────────────────────────────────────────────────────────────────────
193      mk_eq_mk_of_basis h s_basis,
id       └───────────────┘  └─────┘
src  ───┘└───────────────┘ 
typ  ───┘└───────────────┘└─────┘
doc  ───┘└───────────────┘ 
txt  ───┘                  
par  ───┘                  
pid  ───┘                  
st   ──────────────────────────────┘└─
194    rw [A, ← B, lift_nat_cast] at C,
id               └───────────┘
src    └──┘ └──┘ └┘└───────────┘└────┘
typ    └──┘└──┘└┘└───────────┘└────┘
doc    └──┘ └──┘ └┘             └────┘
txt    └──┘ └──┘ └┘             └────┘
par    └──┘ └──┘ └┘             └────┘
pid      └┘ └──┘ └┘             └───┘
st   ──────┘└───┘└─────────────┘└───┘└─
195    have : cardinal.lift.{w v} (cardinal.mk ι) = cardinal.lift.{w v} (findim K V),
id            └───────────┘        └─────────┘     └───────────┘        └────┘  
src    └─────┘└───────────┘└─────┘ └─────────┘ └┘ └───────────┘└─────┘ └────┘  
typ    └─────┘└───────────┘└─────┘ └─────────┘└┘ └───────────┘└─────┘ └────┘
doc    └─────┘└───────────┘└─────┘ └─────────┘ └┘ └───────────┘└─────┘ └────┘  
txt    └─────┘             └─────┘             └┘              └─────┘         
par    └─────┘             └─────┘             └┘              └─────┘         
pid    └───┘└┘             └─────┘             └┘              └─────┘         
st   ──────────────────────────────────────────────────────────────────────────────┘
196      by { simp, exact C },
id                        
src           └──┘  └────┘ 
typ           └──┘  └────┘
doc           └──┘  └────┘ 
txt           └──┘  └────┘ 
par           └──┘  └────┘ 
pid                       
st          └───┘└────────┘└┘
197    exact (lift_inj.mp this).symm
id            └─────────┘ └──┘
src    └────┘ └─────────┘    └─────┘
typ    └────┘ └─────────┘└──┘└─────┘
doc    └────┘                └─────┘
txt    └────┘                └─────┘
par    └────┘                └─────┘
pid                         └───┘└┘
st   ───────────────────────────────┘
198  end
st   └─┘
199  
200  /-- If a submodule has maximal dimension in a finite dimensional space, then it is equal to the
201  whole space. -/
202  lemma eq_top_of_findim_eq [finite_dimensional K V] {S : submodule K V}
id                              └────────────────┘         └───────┘  
src                             └────────────────┘           └───────┘
typ                             └────────────────┘         └───────┘  
doc                             └────────────────┘           └───────┘
203    (h : findim K S = findim K V) : S = ⊤ :=
id          └────┘    └────┘        
src         └────┘      └────┘           
typ         └────┘    └────┘        
doc         └────┘       └────┘
204  begin
st   └─────
205    cases exists_is_basis K S with bS hbS,
id           └─────────────┘  
src    └────┘└─────────────┘  └──────────┘
typ    └────┘└─────────────┘└──────────┘
doc    └────┘                 └──────────┘
txt    └────┘                 └──────────┘
par    └────┘                 └──────────┘
pid                          └──────────┘
st   ──────────────────────────────────────┘└─
206    have : linear_independent K (subtype.val : (subtype.val '' bS : set V) → V),
id            └────────────────┘   └─────────┘               └┘ └┘   └─┘      
src    └─────┘└────────────────┘  └─────────┘└─┘            └┘  └─┘└─┘ └┘  
typ    └─────┘└────────────────┘ └─────────┘└─┘           └┘└┘└─┘└─┘ └┘ 
doc    └─────┘└────────────────┘             └─┘                └─┘    └┘  
txt    └─────┘                               └─┘                └─┘    └┘  
par    └─────┘                               └─┘                └─┘    └┘  
pid    └───┘└┘                               └─┘                └─┘    └┘  
st   ────────────────────────────────────────────────────────────────────────────┘└─
207      from @linear_independent.image_subtype _ _ _ _ _ _ _ _ _
id             └──────────────────────────────┘
src      └───┘ └──────────────────────────────┘└──────────────────
typ      └───┘ └──────────────────────────────┘└──────────────────
doc      └───┘                                 └──────────────────
txt      └───┘                                 └──────────────────
par      └───┘                                 └──────────────────
pid      └───┘                                 └──────────────────
st   ─────────────────────────────────────────────────────────────
208        (submodule.subtype S) hbS.1 (by simp),
id          └───────────────┘   └─┘
src  ─────┘ └───────────────┘ └┘   └─┘   └──┘
typ  ─────┘ └───────────────┘└┘└─┘└─┘   └──┘
doc  ─────┘                   └┘   └─┘   └──┘
txt  ─────┘                   └┘   └─┘   └──┘
par  ─────┘                   └┘   └─┘   └──┘
pid  ─────┘                   └┘   └─┘   └────┘
st   ────────────────────────────────────┘└───┘└─
209    cases exists_subset_is_basis this with b hb,
id           └────────────────────┘ └──┘
src    └────┘└────────────────────┘    └────────┘
typ    └────┘└────────────────────┘└──┘└────────┘
doc    └────┘                          └────────┘
txt    └────┘                          └────────┘
par    └────┘                          └────────┘
pid                                   └────────┘
st   ────────────────────────────────────────────┘└─
210    letI : fintype b := classical.choice (finite_of_linear_independent hb.2.1),
id            └─────┘     └──────────────┘  └──────────────────────────┘ └┘
src    └─────┘└─────┘ └──┘└──────────────┘ └──────────────────────────┘  └───┘
typ    └─────┘└─────┘└──┘└──────────────┘ └──────────────────────────┘└┘└───┘
doc    └─────┘└─────┘ └──┘                                               └───┘
txt    └─────┘        └──┘                                               └───┘
par    └─────┘        └──┘                                               └───┘
pid        └┘        └──┘                                               └───┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
211    letI : fintype (subtype.val '' bS) := classical.choice (finite_of_linear_independent this),
id            └─────┘  └─────────┘    └┘     └──────────────┘  └──────────────────────────┘ └──┘
src    └─────┘└─────┘ └─────────┘    └───┘└──────────────┘ └──────────────────────────┘    
typ    └─────┘└─────┘ └─────────┘  └┘└───┘└──────────────┘ └──────────────────────────┘└──┘
doc    └─────┘└─────┘                └───┘                                                 
txt    └─────┘                       └───┘                                                 
par    └─────┘                       └───┘                                                 
pid        └┘                       └──┘                                                 
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
212    letI : fintype bS := classical.choice (finite_of_linear_independent hbS.1),
id            └─────┘ └┘    └──────────────┘  └──────────────────────────┘ └─┘
src    └─────┘└─────┘  └──┘└──────────────┘ └──────────────────────────┘   └─┘
typ    └─────┘└─────┘└┘└──┘└──────────────┘ └──────────────────────────┘└─┘└─┘
doc    └─────┘└─────┘  └──┘                                                └─┘
txt    └─────┘         └──┘                                                └─┘
par    └─────┘         └──┘                                                └─┘
pid        └┘         └──┘                                                └─┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
213    have : subtype.val '' bS = b, from set.eq_of_subset_of_card_le hb.1
id            └─────────┘    └┘         └─────────────────────────┘ └┘
src    └─────┘└─────────┘       └───┘└─────────────────────────┘  └──
typ    └─────┘└─────────┘  └┘  └───┘└─────────────────────────┘└┘└──
doc    └─────┘                   └───┘                             └──
txt    └─────┘                   └───┘                             └──
par    └─────┘                   └───┘                             └──
pid    └───┘└┘                   └───┘                             └──
st   ─────────────────────────────┘└───────────────────────────────────────
214      (by rw [set.card_image_of_injective _ subtype.val_injective, ← findim_eq_card_basis hbS,
id               └─────────────────────────┘   └───────────────────┘    └──────────────────┘ └─┘
src  ───┘   └──┘└─────────────────────────┘└─┘└───────────────────┘└──┘└──────────────────┘   └─
typ  ───┘   └──┘└─────────────────────────┘└─┘└───────────────────┘└──┘└──────────────────┘└─┘└─
doc  ───┘   └──┘                           └─┘                     └──┘└──────────────────┘   └─
txt  ───┘   └──┘                           └─┘                     └──┘                       └─
par  ───┘   └──┘                           └─┘                     └──┘                       └─
pid  ───┘   └───┘                           └─┘                     └──┘                       └─
st   ──────┘└──────────────────────────────────────────────────────┘└──────────────────────────┘└─
215           ← findim_eq_card_basis hb.2, h]; apply_instance),
id              └──────────────────┘ └┘    
src  ──────────┘└──────────────────┘  └──┘ └┘└────────────┘
typ  ──────────┘└──────────────────┘└┘└──┘└┘└────────────┘
doc  ──────────┘└──────────────────┘  └──┘ └┘└────────────┘
txt  ──────────┘                      └──┘ └┘└────────────┘
par  ──────────┘                      └──┘ └┘└────────────┘
pid  ──────────┘                      └──┘ └────────────────┘
st   ─────────────────────────────────┘└───┘└──────────────┘└─
216    erw [← hb.2.2, subtype.val_range, ← this, set.set_of_mem_eq, ← subtype_eq_val, span_image],
id            └┘      └───────────────┘    └──┘  └───────────────┘    └────────────┘  └────────┘
src    └─────┘  └────┘└───────────────┘└──┘    └┘└───────────────┘└──┘└────────────┘└┘└────────┘
typ    └─────┘└┘└────┘└───────────────┘└──┘└──┘└┘└───────────────┘└──┘└────────────┘└┘└────────┘
doc    └─────┘  └────┘                 └──┘    └┘                 └──┘              └┘          
txt    └─────┘  └────┘                 └──┘    └┘                 └──┘              └┘          
par    └─────┘  └────┘                 └──┘    └┘                 └──┘              └┘          
pid       └──┘  └────┘                 └──┘    └┘                 └──┘              └┘          
st   ────────────┘└───────────────────┘└──────┘└─────────────────┘└────────────────┘└──────────┘└──
217    have := hbS.2,
id             └─┘
src    └──────┘   └┘
typ    └──────┘└─┘└┘
doc    └──────┘   └┘
txt    └──────┘   └┘
par    └──────┘   └┘
pid    └───┘└─┘   └┘
st   ──────────────┘└─
218    erw [subtype.val_range, set.set_of_mem_eq] at this,
id          └───────────────┘  └───────────────┘
src    └───┘└───────────────┘└┘└───────────────┘└───────┘
typ    └───┘└───────────────┘└┘└───────────────┘└───────┘
doc    └───┘                 └┘                 └───────┘
txt    └───┘                 └┘                 └───────┘
par    └───┘                 └┘                 └───────┘
pid       └┘                 └┘                 └──────┘
st   ───────────────────────┘└─────────────────┘└──────┘└─
219    rw [this, map_top (submodule.subtype S), range_subtype],
id         └──┘  └─────┘  └───────────────┘    └───────────┘
src    └──┘    └┘└─────┘ └───────────────┘ └─┘└───────────┘
typ    └──┘└──┘└┘└─────┘ └───────────────┘└─┘└───────────┘
doc    └──┘    └┘                          └─┘             
txt    └──┘    └┘                          └─┘             
par    └──┘    └┘                          └─┘             
pid      └┘    └┘                          └─┘             
st   ─────────┘└─────────────────────────────┘└─────────────┘└──
220  end
st   ──┘
221  
222  variable (K)
223  /-- A field is one-dimensional as a vector space over itself. -/
224  @[simp] lemma findim_of_field : findim K K = 1 :=
id                                   └────┘   
src                                  └────┘     
typ                                  └────┘   
doc    └──┘                          └────┘
225  begin
st   └─────
226    have := dim_of_field K,
id             └──────────┘ 
src    └──────┘└──────────┘
typ    └──────┘└──────────┘
doc    └──────┘            
txt    └──────┘            
par    └──────┘            
pid    └───┘└─┘            
st   ───────────────────────┘└─
227    rw [← findim_eq_dim] at this,
id           └───────────┘
src    └────┘└───────────┘└───────┘
typ    └────┘└───────────┘└───────┘
doc    └────┘└───────────┘└───────┘
txt    └────┘             └───────┘
par    └────┘             └───────┘
pid      └──┘             └──────┘
st   ────────────────────┘└──────┘└─
228    exact_mod_cast this
id                    └──┘
src    └─────────────┘    
typ    └─────────────┘└──┘
doc    └─────────────┘    
txt    └─────────────┘    
par    └─────────────┘    
pid                      
st   ─────────────────────┘
229  end
st   └─┘
230  
231  /-- The vector space of functions on a fintype has finite dimension. -/
232  instance finite_dimensional_fintype_fun {ι : Type*} [fintype ι] :
id                                                        └─────┘ 
src                                                       └─────┘
typ                                                       └─────┘ 
doc                                                       └─────┘
233    finite_dimensional K (ι → K) :=
id     └────────────────┘      
src    └────────────────┘
typ    └────────────────┘      
doc    └────────────────┘
234  by { rw [finite_dimensional_iff_dim_lt_omega, dim_fun'], exact nat_lt_omega _ }
id            └─────────────────────────────────┘  └──────┘         └──────────┘
src       └──┘└─────────────────────────────────┘└┘└──────┘  └────┘└──────────┘└─┘
typ       └──┘└─────────────────────────────────┘└┘└──────┘  └────┘└──────────┘└─┘
doc       └──┘└─────────────────────────────────┘└┘          └────┘            └─┘
txt       └──┘                                   └┘          └────┘            └─┘
par       └──┘                                   └┘          └────┘            └─┘
pid         └┘                                   └┘                           └┘
st     └────────────────────────────────────────┘└────────┘└──────────────────────┘└┘
235  
236  /-- The vector space of functions on a fintype ι has findim equal to the cardinality of ι. -/
237  @[simp] lemma findim_fintype_fun_eq_card {ι : Type v} [fintype ι] :
id                                                          └─────┘ 
src                                                         └─────┘
typ                                                         └─────┘ 
doc    └──┘                                                 └─────┘
238    findim K (ι → K) = fintype.card ι :=
id     └────┘         └──────────┘ 
src    └────┘            └──────────┘
typ    └────┘         └──────────┘ 
doc    └────┘             └──────────┘
239  begin
st   └─────
240    have : vector_space.dim K (ι → K) = fintype.card ι := dim_fun',
id            └──────────────┘           └──────────┘     └──────┘
src    └─────┘└──────────────┘     └┘└──────────┘ └──┘└──────┘
typ    └─────┘└──────────────┘    └┘└──────────┘└──┘└──────┘
doc    └─────┘                     └┘ └──────────┘ └──┘
txt    └─────┘                     └┘              └──┘
par    └─────┘                     └┘              └──┘
pid    └───┘└┘                     └┘              └──┘
st   ───────────────────────────────────────────────────────────────┘└─
241    rwa [← findim_eq_dim, nat_cast_inj] at this,
id            └───────────┘  └──────────┘
src    └─────┘└───────────┘└┘└──────────┘└───────┘
typ    └─────┘└───────────┘└┘└──────────┘└───────┘
doc    └─────┘└───────────┘└┘            └───────┘
txt    └─────┘             └┘            └───────┘
par    └─────┘             └┘            └───────┘
pid       └──┘             └┘            └──────┘
st   ─────────────────────┘└────────────┘└──────┘└─
242  end
st   ──┘
243  
244  /-- The vector space of functions on `fin n` has findim equal to `n`. -/
245  @[simp] lemma findim_fin_fun {n : ℕ} : findim K (fin n → K) = n :=
id                                         └────┘   └─┘       
src                                        └────┘    └─┘        
typ                                        └────┘   └─┘       
doc    └──┘                                 └────┘
246  by simp
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
st     └─────
247  
src  
typ  
doc  
txt  
par  
pid  
st   
248  /-- The submodule generated by a finite set is finite-dimensional. -/
249  theorem span_of_finite {A : set V} (hA : set.finite A) : finite_dimensional K (submodule.span K A) :=
id                               └─┘         └────────┘     └────────────────┘   └────────────┘  
src                              └─┘          └────────┘      └────────────────┘    └────────────┘
typ                              └─┘         └────────┘     └────────────────┘   └────────────┘  
doc                                           └────────┘      └────────────────┘    └────────────┘
250  is_noetherian_span_of_finite K hA
id   └──────────────────────────┘  └┘
src  └──────────────────────────┘
typ  └──────────────────────────┘  └┘
doc  └──────────────────────────┘
251  
252  end finite_dimensional
253  
254  namespace submodule
255  open finite_dimensional
256  
257  /-- A submodule is finitely generated if and only if it is finite-dimensional -/
258  theorem fg_iff_finite_dimensional (s : submodule K V) :
id                                          └───────┘  
src                                         └───────┘
typ                                         └───────┘  
doc                                         └───────┘
259    s.fg ↔ finite_dimensional K s :=
id     └─┘  └────────────────┘  
src     └─┘  └────────────────┘
typ    └─┘  └────────────────┘  
doc           └────────────────┘
260  ⟨λh, is_noetherian_of_fg_of_noetherian s h,
id       └───────────────────────────────┘  
src       └───────────────────────────────┘
typ      └───────────────────────────────┘  
261   λh, by { rw ← map_subtype_top s, exact fg_map (iff_fg.1 h) }⟩
id                 └─────────────┘         └────┘  └────┘   
src            └───┘└─────────────┘   └────┘└────┘ └────┘└─┘ └┘
typ           └───┘└─────────────┘  └────┘└────┘ └────┘└─┘└┘
doc            └───┘└─────────────┘   └────┘       └────┘└─┘ └┘
txt            └───┘                  └────┘             └─┘ └┘
par            └───┘                  └────┘             └─┘ └┘
pid              └─┘                                    └─┘ 
st          └───────────────────────┘└──────────────────────────┘└┘
262  
263  /-- In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding
264  quotient add up to the dimension of the space. -/
265  theorem findim_quotient_add_findim [finite_dimensional K V] (s : submodule K V) :
id                                       └────────────────┘         └───────┘  
src                                      └────────────────┘           └───────┘
typ                                      └────────────────┘         └───────┘  
doc                                      └────────────────┘           └───────┘
266    findim K s.quotient + findim K s = findim K V :=
id     └────┘  └───────┘  └────┘    └────┘  
src    └────┘    └───────┘  └────┘      └────┘
typ    └────┘  └───────┘  └────┘    └────┘  
doc    └────┘    └───────┘   └────┘       └────┘
267  begin
st   └─────
268    have := dim_quotient_add_dim s,
id             └──────────────────┘ 
src    └──────┘└──────────────────┘
typ    └──────┘└──────────────────┘
doc    └──────┘                    
txt    └──────┘                    
par    └──────┘                    
pid    └───┘└─┘                    
st   ───────────────────────────────┘└─
269    rw [← findim_eq_dim, ← findim_eq_dim, ← findim_eq_dim] at this,
id           └───────────┘    └───────────┘    └───────────┘
src    └────┘└───────────┘└──┘└───────────┘└──┘└───────────┘└───────┘
typ    └────┘└───────────┘└──┘└───────────┘└──┘└───────────┘└───────┘
doc    └────┘└───────────┘└──┘└───────────┘└──┘└───────────┘└───────┘
txt    └────┘             └──┘             └──┘             └───────┘
par    └────┘             └──┘             └──┘             └───────┘
pid      └──┘             └──┘             └──┘             └──────┘
st   ────────────────────┘└───────────────┘└───────────────┘└──────┘└─
270    exact_mod_cast this
id                    └──┘
src    └─────────────┘    
typ    └─────────────┘└──┘
doc    └─────────────┘    
txt    └─────────────┘    
par    └─────────────┘    
pid                      
st   ─────────────────────┘
271  end
st   └─┘
272  
273  /-- The dimension of a submodule is bounded by the dimension of the ambient space. -/
274  lemma findim_le [finite_dimensional K V] (s : submodule K V) : findim K s ≤ findim K V :=
id                    └────────────────┘         └───────┘      └────┘    └────┘  
src                   └────────────────┘           └───────┘        └────┘      └────┘
typ                   └────────────────┘         └───────┘      └────┘    └────┘  
doc                   └────────────────┘           └───────┘        └────┘       └────┘
275  by { rw ← s.findim_quotient_add_findim, exact nat.le_add_left _ _ }
id                                                 └─────────────┘
src       └───┘                              └────┘└─────────────┘└───┘
typ       └───┘└──────────────────────────┘  └────┘└─────────────┘└───┘
doc       └───┘                              └────┘               └───┘
txt       └───┘                              └────┘               └───┘
par       └───┘                              └────┘               └───┘
pid         └─┘                                                  └──┘
st     └──────────────────────────────────┘└──────────────────────────┘└┘
276  
277  /-- The dimension of a quotient is bounded by the dimension of the ambient space. -/
278  lemma findim_quotient_le [finite_dimensional K V] (s : submodule K V) :
id                             └────────────────┘         └───────┘  
src                            └────────────────┘           └───────┘
typ                            └────────────────┘         └───────┘  
doc                            └────────────────┘           └───────┘
279    findim K s.quotient ≤ findim K V :=
id     └────┘  └───────┘  └────┘  
src    └────┘    └───────┘  └────┘
typ    └────┘  └───────┘  └────┘  
doc    └────┘    └───────┘   └────┘
280  by { rw ← s.findim_quotient_add_findim, exact nat.le_add_right _ _ }
id                                                 └──────────────┘
src       └───┘                              └────┘└──────────────┘└───┘
typ       └───┘└──────────────────────────┘  └────┘└──────────────┘└───┘
doc       └───┘                              └────┘                └───┘
txt       └───┘                              └────┘                └───┘
par       └───┘                              └────┘                └───┘
pid         └─┘                                                   └──┘
st     └──────────────────────────────────┘└───────────────────────────┘└┘
281  
282  end submodule
283  
284  namespace linear_equiv
285  open finite_dimensional
286  
287  /-- Finite dimensionality is preserved under linear equivalence. -/
288  protected theorem finite_dimensional (f : V ≃ₗ[K] V₂) [finite_dimensional K V] :
id                                              └─┘ └┘   └────────────────┘  
src                                              └─┘       └────────────────┘
typ                                             └─┘ └┘   └────────────────┘  
doc                                              └─┘       └────────────────┘
289    finite_dimensional K V₂ :=
id     └────────────────┘  └┘
src    └────────────────┘
typ    └────────────────┘  └┘
doc    └────────────────┘
290  is_noetherian_of_linear_equiv f
id   └───────────────────────────┘ 
src  └───────────────────────────┘
typ  └───────────────────────────┘ 
291  
292  /-- The dimension of a finite dimensional space is preserved under linear equivalence. -/
293  theorem findim_eq (f : V ≃ₗ[K] V₂) [finite_dimensional K V] :
id                           └─┘ └┘   └────────────────┘  
src                           └─┘       └────────────────┘
typ                          └─┘ └┘   └────────────────┘  
doc                           └─┘       └────────────────┘
294    findim K V = findim K V₂ :=
id     └────┘    └────┘  └┘
src    └────┘      └────┘
typ    └────┘    └────┘  └┘
doc    └────┘       └────┘
295  begin
st   └─────
296    haveI : finite_dimensional K V₂ := f.finite_dimensional,
id             └────────────────┘  └┘    └──────────────────┘
src    └──────┘└────────────────┘   └──┘└──────────────────┘
typ    └──────┘└────────────────┘└┘└──┘└──────────────────┘
doc    └──────┘└────────────────┘   └──┘└──────────────────┘
txt    └──────┘                     └──┘
par    └──────┘                     └──┘
pid         └┘                     └──┘
st   ────────────────────────────────────────────────────────┘└─
297    rcases exists_is_basis_finite K V with ⟨s, s_basis, s_finite⟩,
id            └────────────────────┘  
src    └─────┘└────────────────────┘  └──────────────────────────┘
typ    └─────┘└────────────────────┘└──────────────────────────┘
doc    └─────┘                        └──────────────────────────┘
txt    └─────┘                        └──────────────────────────┘
par    └─────┘                        └──────────────────────────┘
pid                                  └──────────────────────────┘
st   ──────────────────────────────────────────────────────────────┘└─
298    letI : fintype s := s_finite.fintype,
id            └─────┘     └──────────────┘
src    └─────┘└─────┘ └──┘└──────────────┘
typ    └─────┘└─────┘└──┘└──────────────┘
doc    └─────┘└─────┘ └──┘└──────────────┘
txt    └─────┘        └──┘
par    └─────┘        └──┘
pid        └┘        └──┘
st   ─────────────────────────────────────┘└─
299    have A : findim K V = fintype.card s := findim_eq_card_basis s_basis,
id              └────┘    └──────────┘     └──────────────────┘ └─────┘
src    └───────┘└────┘  └──────────┘ └──┘└──────────────────┘
typ    └───────┘└────┘└──────────┘└──┘└──────────────────┘└─────┘
doc    └───────┘└────┘   └──────────┘ └──┘└──────────────────┘
txt    └───────┘                      └──┘                    
par    └───────┘                      └──┘                    
pid    └────┘└─┘                      └──┘                    
st   ─────────────────────────────────────────────────────────────────────┘└─
300    have : is_basis K (λx:s, f (subtype.val x)) := f.is_basis s_basis,
id            └──────┘          └─────────┘        └────────┘ └─────┘
src    └─────┘└──────┘   └┘ └┘  └─────────┘ └────┘└────────┘
typ    └─────┘└──────┘  └┘└┘ └─────────┘ └────┘└────────┘└─────┘
doc    └─────┘└──────┘   └┘ └┘              └────┘          
txt    └─────┘           └┘ └┘              └────┘          
par    └─────┘           └┘ └┘              └────┘          
pid    └───┘└┘           └┘ └┘              └┘└──┘          
st   ──────────────────────────────────────────────────────────────────┘└─
301    have B : findim K V₂ = fintype.card s := findim_eq_card_basis this,
id              └────┘  └┘   └──────────┘     └──────────────────┘ └──┘
src    └───────┘└────┘    └──────────┘ └──┘└──────────────────┘
typ    └───────┘└────┘└┘ └──────────┘└──┘└──────────────────┘└──┘
doc    └───────┘└────┘    └──────────┘ └──┘└──────────────────┘
txt    └───────┘                       └──┘                    
par    └───────┘                       └──┘                    
pid    └────┘└─┘                       └──┘                    
st   ───────────────────────────────────────────────────────────────────┘└─
302    rw [A, B]
id           
src    └──┘ └┘ └┘
typ    └──┘└┘└┘
doc    └──┘ └┘ └┘
txt    └──┘ └┘ └┘
par    └──┘ └┘ └┘
pid      └┘ └┘ 
st   ──────┘└─┘
303  end
st   └─┘
304  
305  end linear_equiv
306  
307  namespace linear_map
308  open finite_dimensional
309  
310  /-- On a finite-dimensional space, an injective linear map is surjective. -/
311  lemma surjective_of_injective [finite_dimensional K V] {f : V →ₗ[K] V}
id                                  └────────────────┘          └─┘ 
src                                 └────────────────┘             └─┘ 
typ                                 └────────────────┘          └─┘ 
doc                                 └────────────────┘
312    (hinj : injective f) : surjective f :=
id             └───────┘     └────────┘ 
src            └───────┘      └────────┘
typ            └───────┘     └────────┘ 
313  begin
st   └─────
314    have h := dim_eq_injective _ hinj,
id               └──────────────┘   └──┘
src    └────────┘└──────────────┘└─┘
typ    └────────┘└──────────────┘└─┘└──┘
doc    └────────┘                └─┘
txt    └────────┘                └─┘
par    └────────┘                └─┘
pid    └────┘└─┘                └─┘
st   ──────────────────────────────────┘└─
315    rw [← findim_eq_dim, ← findim_eq_dim, nat_cast_inj] at h,
id           └───────────┘    └───────────┘  └──────────┘
src    └────┘└───────────┘└──┘└───────────┘└┘└──────────┘└────┘
typ    └────┘└───────────┘└──┘└───────────┘└┘└──────────┘└────┘
doc    └────┘└───────────┘└──┘└───────────┘└┘            └────┘
txt    └────┘             └──┘             └┘            └────┘
par    └────┘             └──┘             └┘            └────┘
pid      └──┘             └──┘             └┘            └───┘
st   ────────────────────┘└───────────────┘└────────────┘└───┘└─
316    exact range_eq_top.1 (eq_top_of_findim_eq h.symm)
id           └──────────┘    └─────────────────┘ └────┘
src    └────┘└──────────┘└─┘ └─────────────────┘└────┘└┘
typ    └────┘└──────────┘└─┘ └─────────────────┘└────┘└┘
doc    └────┘            └─┘ └─────────────────┘      └┘
txt    └────┘            └─┘                          └┘
par    └────┘            └─┘                          └┘
pid                     └─┘                          
st   ───────────────────────────────────────────────────┘
317  end
st   └─┘
318  
319  /-- On a finite-dimensional space, a linear map is injective if and only if it is surjective. -/
320  lemma injective_iff_surjective [finite_dimensional K V] {f : V →ₗ[K] V} :
id                                   └────────────────┘          └─┘ 
src                                  └────────────────┘             └─┘ 
typ                                  └────────────────┘          └─┘ 
doc                                  └────────────────┘
321    injective f ↔ surjective f :=
id     └───────┘   └────────┘ 
src    └───────┘    └────────┘
typ    └───────┘   └────────┘ 
322  ⟨surjective_of_injective,
id    └─────────────────────┘
src   └─────────────────────┘
typ   └─────────────────────┘
doc   └─────────────────────┘
323    λ hsurj, let ⟨g, hg⟩ := exists_right_inverse_linear_map_of_surjective
id       └───┘  └─┘           └───────────────────────────────────────────┘
src                            └───────────────────────────────────────────┘
typ      └───┘  └─┘           └───────────────────────────────────────────┘
324      (range_eq_top.2 hsurj) in
id        └──────────┘  └───┘
src       └──────────┘
typ       └──────────┘  └───┘
325    have function.right_inverse g f,
id          └────────────────────┘   
src         └────────────────────┘
typ         └────────────────────┘   
326      from λ x, show (linear_map.comp f g) x = (@linear_map.id K V _ _ _ : V → V) x, by rw hg,
id                      └─────────────┘         └───────────┘                        └┘
src                      └─────────────┘           └───────────┘                          └─┘
typ                     └─────────────┘         └───────────┘                     └─┘└┘
doc                                                                                        └─┘
txt                                                                                        └─┘
par                                                                                        └─┘
pid                                                                                          
st                                                                                        └────┘
327    injective_of_has_left_inverse ⟨g, left_inverse_of_surjective_of_right_inverse
id     └───────────────────────────┘     └─────────────────────────────────────────┘
src    └───────────────────────────┘     └─────────────────────────────────────────┘
typ    └───────────────────────────┘     └─────────────────────────────────────────┘
328      (surjective_of_injective (injective_of_has_left_inverse ⟨_, this⟩))
id        └─────────────────────┘  └───────────────────────────┘     └──┘
src       └─────────────────────┘  └───────────────────────────┘
typ       └─────────────────────┘  └───────────────────────────┘     └──┘
doc       └─────────────────────┘
329        this⟩⟩
id         └──┘
typ        └──┘
330  
331  lemma ker_eq_bot_iff_range_eq_top [finite_dimensional K V] {f : V →ₗ[K] V} :
id                                      └────────────────┘          └─┘ 
src                                     └────────────────┘             └─┘ 
typ                                     └────────────────┘          └─┘ 
doc                                     └────────────────┘
332    f.ker = ⊥ ↔ f.range = ⊤ :=
id     └──┘    └────┘  
src     └──┘     └────┘  
typ    └──┘    └────┘  
doc     └──┘        └────┘
333  by rw [range_eq_top, ker_eq_bot, injective_iff_surjective]
id          └──────────┘  └────────┘  └──────────────────────┘
src     └──┘└──────────┘└┘└────────┘└┘└──────────────────────┘└─
typ     └──┘└──────────┘└┘└────────┘└┘└──────────────────────┘└─
doc     └──┘            └┘          └┘└──────────────────────┘└─
txt     └──┘            └┘          └┘                        └─
par     └──┘            └┘          └┘                        └─
pid       └┘            └┘          └┘                        
st     └───────────────┘└──────────┘└────────────────────────┘
334  
src  
typ  
doc  
txt  
par  
pid  
st   
335  /-- In a finite-dimensional space, if linear maps are inverse to each other on one side then they
336  are also inverse to each other on the other side. -/
337  lemma mul_eq_one_of_mul_eq_one [finite_dimensional K V] {f g : V →ₗ[K] V} (hfg : f * g = 1) :
id                                   └────────────────┘            └─┘             
src                                  └────────────────┘               └─┘                 
typ                                  └────────────────┘            └─┘             
doc                                  └────────────────┘
338    g * f = 1 :=
id        
src         
typ       
339  have ginj : injective g, from injective_of_has_left_inverse
id               └───────┘        └───────────────────────────┘
src              └───────┘         └───────────────────────────┘
typ              └───────┘        └───────────────────────────┘
340    ⟨f, λ x, show (f * g) x = (1 : V →ₗ[K] V) x, by rw hfg; refl⟩,
id                              └─┘           └─┘
src                                   └─┘           └─┘     └──┘
typ                             └─┘        └─┘└─┘  └──┘
doc                                                    └─┘     └──┘
txt                                                    └─┘     └──┘
par                                                    └─┘     └──┘
pid                                                      
st                                                    └───────────┘
341  let ⟨i, hi⟩ := exists_right_inverse_linear_map_of_surjective
id   └─┘    └┘     └───────────────────────────────────────────┘
src                 └───────────────────────────────────────────┘
typ  └─┘    └┘     └───────────────────────────────────────────┘
342    (range_eq_top.2 (injective_iff_surjective.1 ginj)) in
id      └──────────┘   └──────────────────────┘  └──┘
src     └──────────┘   └──────────────────────┘
typ     └──────────┘   └──────────────────────┘  └──┘
doc                     └──────────────────────┘
343  have f * (g * i) = f * 1, from congr_arg _ hi,
id                           └───────┘
src                             └───────┘
typ                          └───────┘
344  by rw [← mul_assoc, hfg, one_mul, mul_one] at this; rwa ← this
id            └───────┘  └─┘  └─────┘  └─────┘                 └──┘
src     └────┘└───────┘└┘   └┘└─────┘└┘└─────┘└───────┘  └────┘    
typ     └────┘└───────┘└┘└─┘└┘└─────┘└┘└─────┘└───────┘  └────┘└──┘
doc     └────┘         └┘   └┘       └┘       └───────┘  └────┘    
txt     └────┘         └┘   └┘       └┘       └───────┘  └────┘    
par     └────┘         └┘   └┘       └┘       └───────┘  └────┘    
pid       └──┘         └┘   └┘       └┘       └──────┘     └─┘    
st     └──────────────┘└───┘└───────┘└───────┘└────────────────────
345  
src  
typ  
doc  
txt  
par  
pid  
st   
346  /-- In a finite-dimensional space, linear maps are inverse to each other on one side if and only if
347  they are inverse to each other on the other side. -/
348  lemma mul_eq_one_comm [finite_dimensional K V] {f g : V →ₗ[K] V} : f * g = 1 ↔ g * f = 1 :=
id                          └────────────────┘            └─┘               
src                         └────────────────┘               └─┘                     
typ                         └────────────────┘            └─┘               
doc                         └────────────────┘
349  ⟨mul_eq_one_of_mul_eq_one, mul_eq_one_of_mul_eq_one⟩
id    └──────────────────────┘  └──────────────────────┘
src   └──────────────────────┘  └──────────────────────┘
typ   └──────────────────────┘  └──────────────────────┘
doc   └──────────────────────┘  └──────────────────────┘
350  
351  /-- In a finite-dimensional space, linear maps are inverse to each other on one side if and only if
352  they are inverse to each other on the other side. -/
353  lemma comp_eq_id_comm [finite_dimensional K V] {f g : V →ₗ[K] V} : f.comp g = id ↔ g.comp f = id :=
id                          └────────────────┘            └─┘     └───┘   └┘  └───┘   └┘
src                         └────────────────┘               └─┘        └───┘    └┘   └───┘    └┘
typ                         └────────────────┘            └─┘     └───┘   └┘  └───┘   └┘
doc                         └────────────────┘
354  mul_eq_one_comm
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
doc  └─────────────┘
355  
356  /-- The image under an onto linear map of a finite-dimensional space is also finite-dimensional. -/
357  lemma finite_dimensional_of_surjective [h : finite_dimensional K V]
id                                               └────────────────┘  
src                                              └────────────────┘
typ                                              └────────────────┘  
doc                                              └────────────────┘
358    (f : V →ₗ[K] V₂) (hf : f.range = ⊤) : finite_dimensional K V₂ :=
id           └─┘ └┘        └────┘      └────────────────┘  └┘
src           └─┘             └────┘      └────────────────┘
typ          └─┘ └┘        └────┘      └────────────────┘  └┘
doc                            └────┘        └────────────────┘
359  is_noetherian_of_surjective V f hf
id   └─────────────────────────┘   └┘
src  └─────────────────────────┘
typ  └─────────────────────────┘   └┘
360  
361  /-- The range of a linear map defined on a finite-dimensional space is also finite-dimensional. -/
362  instance finite_dimensional_range [h : finite_dimensional K V] (f : V →ₗ[K] V₂) :
id                                          └────────────────┘          └─┘ └┘
src                                         └────────────────┘             └─┘ 
typ                                         └────────────────┘          └─┘ └┘
doc                                         └────────────────┘
363    finite_dimensional K f.range :=
id     └────────────────┘  └────┘
src    └────────────────┘    └────┘
typ    └────────────────┘  └────┘
doc    └────────────────┘    └────┘
364  f.quot_ker_equiv_range.finite_dimensional
id   └───────────────────┘└─────────────────┘
src   └───────────────────┘└─────────────────┘
typ  └───────────────────┘└─────────────────┘
doc   └───────────────────┘└─────────────────┘
365  
366  /-- rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to
367  the dimension of the source space. -/
368  theorem findim_range_add_findim_ker [finite_dimensional K V] (f : V →ₗ[K] V₂) :
id                                        └────────────────┘          └─┘ └┘
src                                       └────────────────┘             └─┘ 
typ                                       └────────────────┘          └─┘ └┘
doc                                       └────────────────┘
369    findim K f.range + findim K f.ker = findim K V :=
id     └────┘  └────┘  └────┘  └──┘  └────┘  
src    └────┘    └────┘  └────┘    └──┘  └────┘
typ    └────┘  └────┘  └────┘  └──┘  └────┘  
doc    └────┘    └────┘   └────┘    └──┘   └────┘
370  by { rw [← f.quot_ker_equiv_range.findim_eq], exact submodule.findim_quotient_add_findim _ }
id                                                       └──────────────────────────────────┘
src       └────┘                                  └────┘└──────────────────────────────────┘└─┘
typ       └────┘└──────────────────────────────┘  └────┘└──────────────────────────────────┘└─┘
doc       └────┘                                  └────┘└──────────────────────────────────┘└─┘
txt       └────┘                                  └────┘                                    └─┘
par       └────┘                                  └────┘                                    └─┘
pid         └──┘                                                                           └┘
st     └───────────────────────────────────────┘└──────────────────────────────────────────────┘└┘
371  
372  end linear_map